|
|
Generátor testovacích dat pro databáze finančních technologií
Moresová, Eva ; Vašíček, Ondřej (oponent) ; Smrčka, Aleš (vedoucí práce)
Táto bakalárska práca sa zaoberá vytvorením generátora testovacích dát pre databázy aplikácií z oblasti finančných technológií. Riešenie tohto problému bolo realizované ako rozšírenie a upravenie funkcionality existujúceho nástroja dbgenx, ktorý je súčasťou platformy Testos. Vytvorený nástroj umožňuje generovať dáta s ohľadom na ich štrukturálne a sémantické závislosti, definovať vlastné externé moduly na generovanie a poskytuje efektívny zápis predpisu pre generované dáta.
|
|
| |
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
|
|
|
Rozvoj nástroje Combine
Nováček, Pavel ; Janoušek, Vladimír (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá reimplementací webového nástroje Combine, který pro uživatelem specifikované parametry a specifikovaná omezení vygeneruje použitím algoritmu IPOG kombinatorickou testovací sadu splňující požadované kombinatorické kritérium pokrytí. Práce je řešena v kontextu platformy Testos, která cílí na automatizaci softwarového testování. Cílem této práce je analyzovat aktuální stav nástroje, identifikovat jeho chyby a nedostatky, diskutovat vhodná rozšíření jeho funkcionality a na základě těchto poznatků vytvořit nový návrh a implementaci nástroje Combine. Vytvořené řešení zachovává veškerou funkcionalitu původního nástroje a zároveň ji rozšiřuje na všech úrovních architektury. Nástroj je nejen lépe ovladatelný díky uživatelsky přívětivějšímu webovému rozhraní, ale nabízí i nové možnosti pro generování testovacích sad. Pro jeho implementaci byly zvoleny vhodnější technologie, díky kterým je nástroj přenositelný a generuje testovací sadu značně rychleji než předchozí implementace a dokáže konkurovat existujícím řešením pro generování kombinatorické testovací sady.
|
|
|
Generátor testovacích dat pro databáze finančních technologií
Moresová, Eva ; Vašíček, Ondřej (oponent) ; Smrčka, Aleš (vedoucí práce)
Táto bakalárska práca sa zaoberá vytvorením generátora testovacích dát pre databázy aplikácií z oblasti finančných technológií. Riešenie tohto problému bolo realizované ako rozšírenie a upravenie funkcionality existujúceho nástroja dbgenx, ktorý je súčasťou platformy Testos. Vytvorený nástroj umožňuje generovať dáta s ohľadom na ich štrukturálne a sémantické závislosti, definovať vlastné externé moduly na generovanie a poskytuje efektívny zápis predpisu pre generované dáta.
|
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
|
|
| |
host ::
RSS.